Nuprl Lemma : chain-order-in-out 13,45

es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), SysOut:AbsInterface(Top).
(E(Inr E(Sys))
 (E(Outr E(Sys))
 (f:sys-antecedent(es;Sys), chain:(E(Sys)(Id List)).
 chain-consistent(f;chain)
  (e:E(In), e':E(Out). ((isupdate(In(e))))  loc(e) <<= loc(e'))) 
latex


Upabstract chain replication
Definitionst  T, left + right, P  Q, Dec(P), x:AB(x), x:AB(x), IdLnk, (x  l), P  Q, l_disjoint(T;l1;l2), Knd, MaName, E, (e <loc e'), e loc e' , (e < e'), e c e', x:A  B(x), x:AB(x), e<e'.P(e), ee'.P(e), e<e'P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), b, e  X, ES, Type, AbsInterface(A), , sys-antecedent(es;Sys), type List, a < b, no_repeats(T;l), P & Q, L1  L2, <ab>, adjacent(T;L;x;y), E(X), {x:AB(x)} , False, A, increasing(f;k), let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), Top, ||as||, #$n, , True, T, b | a, a ~ b, a  b, a <p b, a < b, A c B, x f y, xLP(x), (xL.P(x)), r  s, r < s, q-rel(r;x), Outcome, SqStable(P), P  Q, a =!x:TQ(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a  b, IsIntegDom(r), IsPrimeIdeal(R;P), strong-subtype(A;B), f  g, chain-consistent(f;chain), ff, b, tt, x <<= y, p =b q, i <z j, i j, (i = j), x =a y, null(as), a < b, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p  q, p  q, p q, {T}, SQType(T), s ~ t, EState(T), a:A fp B(a), , EqDecider(T), Unit, EOrderAxioms(Epred?info), kindcase(ka.f(a); l,t.g(l;t) ), loc(e), kind(e), Msg(M), , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'), x,yt(x;y), !Void(), x:A.B(x), S  T, suptype(ST), first(e), pred(e), x.A(x), xt(x), x  dom(f), loc(e), Id, s = t, f(a), last(L), hd(l), X(e), if b then t else f fi , x << y, x before y  l, Atom$n, l[i], [car / cdr], P  Q
Lemmashd-before, member sublist, before last, es-loc wf, l member subtype, false wf, Id sq, l before wf, chain-order wf, es-interface-val wf2, chain-consistent wf, es-causle wf, sys-antecedent wf, es-interface wf, es-E-interface wf, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, first wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf, bool cases, eqtt to assert, guard wf, bool sq, iff transitivity, eqff to assert, assert of bnot, chain-order-le wf, bool wf, bnot wf, not wf, sq stable from decidable, decidable assert, assert wf, es-is-interface wf, top wf, decidable equal Id

origin